import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import org.junit.jupiter.api.Test;
import proof.ConclusionProof;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.ArrayList;

import static org.junit.jupiter.api.Assertions.*;

class ProofRuleTest {

    @Test
    void D1ST() {//{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        Formula c=new UnaryFormula(new UnaryLiteral(new UnaryAtom("c"),false));
        Formula d=new UnaryFormula(new UnaryLiteral(new UnaryAtom("d"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,a,b);
        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,b,c);
        //BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,a,c);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(f2));
        proofs.add(new ConclusionProof(f1));
        Proof result=new DerivedProof(proofs,ProofRule.D1);

        String expected="[{ANY(b,c),Exist(a,b)}D1 -> Exist(a,c)]";

       assertEquals(expected,result.toString());
    }

    @Test
    void D1MT() {//{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        Formula n=new UnaryFormula(new UnaryLiteral(new UnaryAtom("n"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,l);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,q);
        BinaryFormula f3=new BinaryFormula(FormulaSign.ANY,l,n);

        //测试solveHelper
        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,p,n);
        ArrayList<Formula> arrayList=new ArrayList<>();
        arrayList.add(f1);
        arrayList.add(f2);
        arrayList.add(f3);
        Proof result=Solve.solve(arrayList,conclusion);

        String expected="[{ANY(l,n),[{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)]}D1 -> Exist(p,n)]";
        //System.out.println(Solve.solve(arrayList,conclusion));
        assertEquals(expected,result.toString());
    }
}